Search Results

Documents authored by Fuenmayor, David


Document
Value-Oriented Legal Argumentation in Isabelle/HOL

Authors: Christoph Benzmüller and David Fuenmayor

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)


Abstract
Literature in AI & Law contemplates argumentation in legal cases as an instance of theory construction. The task of a lawyer in a legal case is to construct a theory containing: (a) relevant generic facts about the world, (b) relevant legal rules such as precedents and statutes, and (c) contingent facts describing or interpreting the situation at hand. Lawyers then elaborate convincing arguments starting from these facts and rules, deriving into a positive decision in favour of their client, often employing sophisticated argumentation techniques involving such notions as burden of proof, stare decisis, legal balancing, etc. In this paper we exemplarily show how to harness Isabelle/HOL to model lawyer’s argumentation using value-oriented legal balancing, while drawing upon shallow embeddings of combinations of expressive modal logics in HOL. We highlight the essential role of model finders (Nitpick) and "hammers" (Sledgehammer) in assisting the task of legal theory construction and share some thoughts on the practicability of extending the catalogue of ITP applications towards legal informatics.

Cite as

Christoph Benzmüller and David Fuenmayor. Value-Oriented Legal Argumentation in Isabelle/HOL. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{benzmuller_et_al:LIPIcs.ITP.2021.7,
  author =	{Benzm\"{u}ller, Christoph and Fuenmayor, David},
  title =	{{Value-Oriented Legal Argumentation in Isabelle/HOL}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.7},
  URN =		{urn:nbn:de:0030-drops-139028},
  doi =		{10.4230/LIPIcs.ITP.2021.7},
  annote =	{Keywords: Higher order logic, preference logic, shallow embedding, legal reasoning}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail